perm filename HOMEW2.XGP[206,LSP]1 blob
sn#386969 filedate 1978-10-05 generic text, type T, neo UTF8
/LMAR=0/XLINE=3/FONT#0=BAXL30[FNT,CLT]/FONT#1=BAXM30/FONT#2=BAXB30[FNT,CLT]/FONT#5=GACS25
␈↓ ↓H␈↓␈↓ ¬πSTANFORD UNIVERSITY
␈↓ ↓H␈↓CS206 ␈↓ βZCOMPUTING WITH SYMBOLIC EXPRESSIONS ␈↓
SPRING 1978
␈↓ ↓H␈↓␈↓ ¬DPROBLEM SET 2
␈↓ ↓H␈↓␈↓ ¬rDue May 16
␈↓ ↓H␈↓αGeneral comments.
␈↓ ↓H␈↓ This␈α⊂assignment␈α⊂involves␈α∂proving␈α⊂properties␈α⊂of␈α∂LISP␈α⊂functions.␈α⊂ Unless␈α⊂otherwise␈α∂noted
␈↓ ↓H␈↓your␈α∪proofs␈α∪should␈α∪be␈α∪fairly␈α∪formal.␈α∪ The␈α∪level␈α∪of␈α∪detail␈α∪should␈α∪be␈α∪approximately␈α∀that␈α∪of
␈↓ ↓H␈↓Chapter III␈αsection 7␈αof␈αthe␈αnotes.␈α For␈αeach␈αstep␈αof␈αyour␈αproof,␈αmake␈αsure␈αthat␈αyou␈αlist␈αall␈αof␈αthe
␈↓ ↓H␈↓facts␈α
(axioms,␈αearlier␈α
steps␈α
or␈αpreviously␈α
proved␈α
properties)␈αthat␈α
are␈α
necessary␈αto␈α
make␈α
that␈αstep.
␈↓ ↓H␈↓You may use any facts already proved in the notes or in class.
␈↓ ↓H␈↓αAssignment.
␈↓ ↓H␈↓1. Chapter III. Exercise 1. ii-v.
␈↓ ↓H␈↓2. Chapter III. Exercise 2.
␈↓ ↓H␈↓3.␈α
EXTRA␈α(for␈α
practice␈α
with␈αextended␈α
truth␈αvalues,␈α
not␈α
required).␈α Let␈α
␈↓↓andlist␈↓␈αbe␈α
as␈α
defined␈αin
␈↓ ↓H␈↓␈↓ α(Chapter I and assume ␈↓↓p␈↓ is a suitably well-behaved predicate. Prove the following:
␈↓ ↓H␈↓ 3.1. ␈↓↓∀u v: [andlis[u*v, p] = andlis[u, p] ∧ andlis[v, p]]␈↓
␈↓ ↓H␈↓ 3.2. ␈↓↓∀u: [andlis[reverse u, p] = andlis[u, p]]␈↓
␈↓ ↓H␈↓Hint:␈αdefine␈α␈↓↓aandlis,␈↓␈αwhich␈αreturns␈αan␈αextended␈αtruth␈αvalue␈αcorresponding␈αto␈αthe␈αtruth␈αvalue␈αof
␈↓ ↓H␈↓␈↓ α(␈↓↓andlis␈↓␈α⊃on␈α⊃corresponding␈α⊃arguments.␈α⊃ Show␈α⊃that␈α⊃␈↓↓andlis␈α⊃as␈↓␈α⊃defined␈α⊃in␈α⊃terms␈α∩of␈α⊃␈↓↓aandlis␈↓
␈↓ ↓H␈↓␈↓ α(satisfies␈αthe␈αdesired␈αequivalence.␈α Then␈αyou␈αmay␈αuse␈αthis␈αresult␈αto␈αprove␈αother␈αfacts␈αabout
␈↓ ↓H␈↓␈↓ α(␈↓↓andlis.␈↓␈α The␈α
statement␈αthat␈α
"␈↓↓p␈↓␈αis␈αsuitably␈α
well-behaved"␈αis␈α
rather␈αvague.␈α
You␈αwill␈αneed␈α
to
␈↓ ↓H␈↓␈↓ α(make it more precise in order to make your proof clear. State this in your proof.
␈↓ ↓H␈↓␈↓ ∧+COMPUTER SCIENCE DEPARTMENT
␈↓ ↓H␈↓␈↓ ¬πSTANFORD UNIVERSITY
␈↓ ↓H␈↓CS206 ␈↓ βZCOMPUTING WITH SYMBOLIC EXPRESSIONS ␈↓
+Spring 1978
␈↓ ↓H␈↓α␈↓ ¬
Solutions for Problem Set 2.
␈↓ ↓H␈↓αGeneral comments.
␈↓ ↓H␈↓ The␈α∞following␈α∞proofs␈α∂are␈α∞generally␈α∞informal␈α∞and␈α∂emphasize␈α∞mainly␈α∞the␈α∞details␈α∂which␈α∞are
␈↓ ↓H␈↓most␈αfrequently␈αmissed.␈α
In␈αparticular,␈αsince␈α
the␈αaxioms␈αand␈α
theorems␈αare␈αstated␈α
in␈αterms␈αof␈α
sorted
␈↓ ↓H␈↓variables␈αit␈α
is␈αimportant␈αto␈α
understand␈αthe␈αimplications␈α
of␈αthis␈α
in␈αorder␈αnot␈α
to␈αprove␈αthings␈α
which
␈↓ ↓H␈↓are␈αin␈αfact␈αfalse.␈α Thus␈αcare␈αhas␈αbeen␈αtaken␈α to␈αpoint␈αout␈αwhere␈αit␈αis␈αthat␈αterms␈αhave␈αto␈αbe␈αshown
␈↓ ↓H␈↓to␈α∪be␈α∪of␈α∪a␈α∪given␈α∩sort␈α∪in␈α∪order␈α∪that␈α∪the␈α∩axioms,␈α∪definitions,␈α∪and␈α∪theorems␈α∪can␈α∪be␈α∩applied.
␈↓ ↓H␈↓Problem 3␈αis␈αworked␈α
out␈αin␈αsome␈α
detail␈αin␈αorder␈αto␈α
provide␈αan␈αadditional␈α
example␈αof␈αthe␈α
use␈αof
␈↓ ↓H␈↓representing␈α⊂functions␈α∂and␈α⊂extended␈α⊂truthvalues␈α∂to␈α⊂prove␈α∂statements␈α⊂about␈α⊂recursively␈α∂defined
␈↓ ↓H␈↓predicates.
␈↓ ↓H␈↓ The␈α∞proofs␈α
will␈α∞be␈α
fairly␈α∞brief␈α
in␈α∞other␈α
respects␈α∞and␈α
in␈α∞particular␈α
the␈α∞basic␈α∞LISP␈α
axioms␈↓ ↓H␈↓␈↓ εH␈↓ 91
␈↓ ↓H␈↓will␈αoften␈α
used␈αwithout␈α
comment.␈α For␈α
example,␈αwe␈α
will␈αgenerally␈α
use␈αthe␈α
fact␈αthat␈α
␈↓↓issexp␈αqa␈αu␈↓␈α
and
␈↓ ↓H␈↓␈↓↓issexp␈α∞qd␈α∞u␈↓␈α∂in␈α∞the␈α∞case␈α∂that␈α∞␈↓↓¬qn␈α∞u␈↓␈α∞without␈α∂explicit␈α∞mention.␈α∞ We␈α∂will␈α∞sometimes␈α∞justify␈α∂a␈α∞step
␈↓ ↓H␈↓saying␈α∩"by␈α∩definition"␈α∩ which␈α∩means␈α∪by␈α∩using␈α∩the␈α∩functional␈α∩equation␈α∩defining␈α∪the␈α∩relevant
␈↓ ↓H␈↓function. Some simplification (of conditional terms etc.) is usually needed to complete the step.
␈↓ ↓H␈↓ Most␈α
of␈α
the␈α
proofs␈α
are␈α
done␈α
by␈α
list␈α
or␈α
S-expression␈α
induction.␈α
For␈α
example,␈α∞suppose␈α
you
␈↓ ↓H␈↓wish␈α
to␈α∞prove␈α
some␈α∞property␈α
␈↓↓qP[u]␈↓␈α∞for␈α
all␈α
lists␈α∞␈↓↓u.␈↓␈α
You␈α∞first␈α
show␈α∞that␈α
qP[qNIL]␈α∞holds.␈α
Then
␈↓ ↓H␈↓you␈αassume␈α
that␈α␈↓↓u␈↓␈α
is␈αnot␈αqNIL␈α
and␈αthat␈α
␈↓↓qP[qd␈αu]␈↓␈αholds␈α
and␈αshow␈α
that␈αunder␈α
these␈αassumptions
␈↓ ↓H␈↓␈↓↓qP[u]␈↓␈α⊃is␈α⊃true.␈α⊃ The␈α⊃fact␈α⊃that␈α⊃␈↓↓qP[u]␈↓␈α⊃holds␈α⊃for␈α⊃all␈α⊃lists␈α⊃␈↓↓u␈↓␈α⊃then␈α⊃follows␈α⊃by␈α⊃list␈α⊃induction.␈α⊂ The
␈↓ ↓H␈↓situation for S-expression induction is analogous.
␈↓ ↓H␈↓αProblem 1.
␈↓ ↓H␈↓ We will use the following facts about the operator < >:
␈↓ ↓H␈↓1.0 ␈↓↓∀x: islist <x>␈↓ and ␈↓↓∀x u: <x> * u = x . u␈↓
␈↓ ↓H␈↓These␈αfacts␈α
are␈αa␈α
simple␈αconsequence␈α
of␈αthe␈α
definitions␈αof␈α
*,␈α<>␈α
and␈αthe␈α
LISP␈αaxioms.␈α
We␈αwill
␈↓ ↓H␈↓also use the result of Problem 1.i which was proved in class.
␈↓ ↓H␈↓αProof of 1.ii ␈↓↓∀u: islist reverse1 u␈↓α
␈↓ ↓H␈↓Method: list induction with ␈↓↓qP[u] ≡ islist reverse1 u␈↓.
␈↓ ↓H␈↓Case ␈↓↓qn u␈↓:
␈↓ ↓H␈↓ ␈↓↓islist reverse1 u ≡ islist qNIL␈↓ ...by definition of ␈↓↓reverse1␈↓
␈↓ ↓H␈↓ ≡ T ...by the LISP axioms.
␈↓ ↓H␈↓Case ␈↓↓¬qn u␈↓ and ␈↓↓islist reverse1 qd u␈↓
␈↓ ↓H␈↓ ␈↓↓islist reverse1 u ≡ islist [reverse1 qd u * <qa u>]␈↓ ...by definition of ␈↓↓reverse1␈↓
␈↓ ↓H␈↓ ≡ T ...by induction hypothesis, ␈↓¬ISLIST-APPEND ␈↓and 1.0.
␈↓ ↓H␈↓αProof of 1.iii ␈↓↓∀u: reverse u = reverse1 u␈↓α
␈↓ ↓H␈↓ We prove a slightly more general result, namely
␈↓ ↓H␈↓1.1 ␈↓↓∀u v: reverse1 u * v = rev[u,v]␈↓
␈↓ ↓H␈↓then taking ␈↓↓v␈↓ = qNIL the desired result follows by 1.i and the definition of ␈↓↓reverse.␈↓
␈↓ ↓H␈↓Method: list induction with ␈↓↓qP[u] ≡ ∀v: reverse1 u * v = rev[u,v]␈↓.
␈↓ ↓H␈↓Case ␈↓↓qn u␈↓
␈↓ ↓H␈↓ ␈↓↓reverse1 qNIL * v = v␈↓ ...by definition of ␈↓↓reverse1␈↓ and ␈↓¬NIL-APPEND ␈↓
␈↓ ↓H␈↓ ␈↓↓= rev[u,v]␈↓ ...by definition of ␈↓↓rev␈↓ .
␈↓ ↓H␈↓Case ␈↓↓¬qn u␈↓ and ␈↓↓∀v: reverse1 qd u * v = rev[qd u,v]␈↓:
␈↓ ↓H␈↓ ␈↓↓reverse1 u = reverse1 qd u * <qa u>␈↓ ...by definition
␈↓ ↓H␈↓ ␈↓↓= rev[qd u,<qa u>]␈↓ ...by induction hypothesis and ␈↓↓islist <qa u>␈↓␈↓ ↓H␈↓␈↓ εH␈↓ 92
␈↓ ↓H␈↓ ␈↓↓= rev[u,qNIL]␈↓ ...by definition.
␈↓ ↓H␈↓ From␈α⊂here␈α⊃on␈α⊂we␈α⊂shall␈α⊃use␈α⊂␈↓↓reverse␈↓␈α⊂and␈α⊃␈↓↓reverse1␈↓␈α⊂interchangably.␈α⊂ As␈α⊃1.iv␈α⊂is␈α⊃more␈α⊂easily
␈↓ ↓H␈↓proved using 1.v, we will prove 1.v next.
␈↓ ↓H␈↓αProof of 1.v ␈↓↓∀u v: reverse[u * v] = reverse v * reverse u␈↓α
␈↓ ↓H␈↓Method: list induction with ␈↓↓qP[u] ≡ ∀v: reverse[u * v] = reverse v * reverse u␈↓.
␈↓ ↓H␈↓Case ␈↓↓qn u␈↓:
␈↓ ↓H␈↓ ␈↓↓reverse[qNIL * v] = reverse v␈↓ ...by ␈↓¬NIL-APPEND ␈↓
␈↓ ↓H␈↓ ␈↓↓= reverse v * qNIL␈↓ ...by 1.i
␈↓ ↓H␈↓ ␈↓↓= reverse v * reverse qNIL␈↓ ...by definition.
␈↓ ↓H␈↓Case ␈↓↓¬qn u␈↓ and ␈↓↓∀v: reverse[qd u * v] = reverse v * reverse qd u␈↓:
␈↓ ↓H␈↓ ␈↓↓reverse[u * v] = reverse[qd u * v] * <qa u>␈↓ ...by definition, ␈↓¬CAR/CDR-APPEND ␈↓and ␈↓↓islist u*v␈↓
␈↓ ↓H␈↓ ␈↓↓= [reverse v * reverse qd u] * <qa u>␈↓ ...by induction hypothesis
␈↓ ↓H␈↓ ␈↓↓= reverse v * [reverse qd u * <qa u>]␈↓ ...by ␈↓¬ASSOC-APPEND ␈↓
␈↓ ↓H␈↓ ...here we need ␈↓↓islist reverse v␈↓, ␈↓↓islist reverse qd u␈↓ and ␈↓↓islist <qa u>␈↓
␈↓ ↓H␈↓ ␈↓↓= reverse v * reverse u␈↓ ...by definition
␈↓ ↓H␈↓αProof of 1.iv ␈↓↓∀u: reverse reverse u = u␈↓α
␈↓ ↓H␈↓Method: list induction with ␈↓↓qP[u] ≡ reverse reverse u = u␈↓.
␈↓ ↓H␈↓Case ␈↓↓qn u␈↓:
␈↓ ↓H␈↓ ␈↓↓reverse reverse qNIL = reverse qNIL = qNIL␈↓ ... by definition
␈↓ ↓H␈↓Case ␈↓↓¬qn u␈↓ and ␈↓↓reverse reverse qd u = qd u␈↓:
␈↓ ↓H␈↓ ␈↓↓reverse reverse u = reverse[reverse qd u * <qa u>]␈↓ ...by definition
␈↓ ↓H␈↓ ␈↓↓= reverse <qa u> * reverse reverse qd u␈↓ ... by 1.v
␈↓ ↓H␈↓ ...here we need ␈↓↓islist reverse qd u␈↓ and ␈↓↓islist <qa u>␈↓
␈↓ ↓H␈↓ ␈↓↓= <qa u> * qd u␈↓ ...by induction hypothesis and computation using ␈↓↓islist <qa u>␈↓
␈↓ ↓H␈↓ ␈↓↓= u␈↓ ...by 1.0 and the LISP axioms
␈↓ ↓H␈↓This␈αends␈αProblem␈α1␈αas␈αassigned.␈α The␈αproof␈αof␈αthe␈αequivalence␈αof␈α␈↓↓flatten␈↓␈αand␈α␈↓↓fringe␈↓␈αas␈αoutlined
␈↓ ↓H␈↓in class is included here for completeness.
␈↓ ↓H␈↓αProof ␈↓↓∀x u: flat[x,u] = fringe x * u␈↓α
␈↓ ↓H␈↓Method: S-expression induction with ␈↓↓qP[x] ≡ ∀u: flat[x,u] = fringe x * u␈↓.
␈↓ ↓H␈↓Case ␈↓↓qat x␈↓:
␈↓ ↓H␈↓ ␈↓↓flat[x,u] = x . u␈↓ ...by definition
␈↓ ↓H␈↓ ␈↓↓= <x> * u␈↓ ... by 1.0
␈↓ ↓H␈↓ ␈↓↓= fringe x * u␈↓ ... by definition
␈↓ ↓H␈↓Case ␈↓↓¬qat x␈↓ and ␈↓↓∀u: flat[qd x,u] = fringe qd x * u␈↓ :
␈↓ ↓H␈↓ ␈↓↓flat[x,u] = flat[qa x,flat[qd x,u]]␈↓ ...by definition␈↓ ↓H␈↓␈↓ εH␈↓ 93
␈↓ ↓H␈↓ ␈↓↓= flat[qa x,fringe qd x * u]␈↓ ...by induction hypothesis
␈↓ ↓H␈↓ ␈↓↓= fringe qa x * [fringe qd x * u]␈↓ ...again by induction hypothesis
␈↓ ↓H␈↓ ...here we need ␈↓↓islist fringe qd x * u␈↓
␈↓ ↓H␈↓ ␈↓↓= fringe x * u␈↓ ...by ␈↓¬ISTOT-APPEND ␈↓and definition of ␈↓↓fringe␈↓
␈↓ ↓H␈↓ ...here we need ␈↓↓islist fringe qd x ␈↓ and ␈↓↓islist fringe qa x␈↓
␈↓ ↓H␈↓αProblem 2.
␈↓ ↓H␈↓ In␈α
proving␈α
the␈α
desired␈α
fact␈α
about␈α
␈↓↓subst,␈↓␈α
␈↓↓sublis,␈↓␈α
and␈α
@␈α
we␈α
will␈α
use␈α
a␈α
new␈α
sort␈α∞␈↓↓slist.␈↓␈α
The
␈↓ ↓H␈↓variables␈α∀␈↓↓s,␈↓␈α∀␈↓↓s1,␈↓␈α∪␈↓↓s2,␈↓␈α∀␈↓↓s3␈↓␈α∀range␈α∀over␈α∪the␈α∀domain␈α∀characterized␈α∪by␈α∀the␈α∀predicate␈α∀␈↓↓slist.␈↓␈α∪ We
␈↓ ↓H␈↓axiomatize slists as follows:
␈↓ ↓H␈↓2.1 ␈↓↓∀X: [slist X ≡ islist X ∧ [qn X ∨ [¬qat qa X ∧ slist qd X]]]␈↓ ...X is a general variable.
␈↓ ↓H␈↓Thus ␈↓↓s␈↓ is either qNIL or a list of nonatomic elements. We shall also use the following facts.
␈↓ ↓H␈↓2.2 ␈↓↓∀x y: [occur[x,y] ≡ [x=y] ∨ [¬qat y ∧ [occur[x, qa y] ∨ occur[x,qd y]]]]␈↓
␈↓ ↓H␈↓2.3 ␈↓↓∀x s: [qn assoc[x,s] ∨ [issexp assoc[x,s] ∧ ¬qat assoc[x,s]]]␈↓
␈↓ ↓H␈↓2.4 ␈↓↓∀s1 s2: slist s1 * s2␈↓
␈↓ ↓H␈↓2.5 ␈↓↓∀z s1 s2: [assoc[z,s1*s2] = qif qn assoc[z,s1] qthen assoc[z,s2] qelse assoc[z,s1]]␈↓
␈↓ ↓H␈↓2.6 ␈↓↓∀x y z: issexp subst[x, y, z]␈↓
␈↓ ↓H␈↓2.7 ␈↓↓∀x,s: issexp sublis[x,s]␈↓
␈↓ ↓H␈↓2.8 ␈↓↓∀s1 s2: slist subsub[s1,s2]␈↓
␈↓ ↓H␈↓ ␈↓↓∀s1 s2: ¬qn s1 ⊃ ¬qn subsub[s1,s2]␈↓
␈↓ ↓H␈↓ ␈↓↓∀s1 s2: ¬qn s1 ⊃ qd subsub[s1,s2] = subsub[qd s1,s2]␈↓
␈↓ ↓H␈↓2.9 ␈↓↓∀s1 s2: slist s1@s2␈↓
␈↓ ↓H␈↓The␈αproof␈αof␈α2.2␈αis␈αoutlined␈αin␈α
the␈αtext␈αand␈α2.3␈α-␈α2.9␈αcan␈α
be␈αproved␈αby␈αstraight␈αforward␈αlist␈αor␈α
S-
␈↓ ↓H␈↓expression induction using the LISP axioms function definitions and 2.1.
␈↓ ↓H␈↓αProof of 2.i ␈↓↓∀x y z: subst[x, y, z] = sublis[z, <x,y>]␈↓α
␈↓ ↓H␈↓Method: S-expression induction with ␈↓↓qP[z] ≡ ∀x y: subst[x,y,z] = sublis[z,<x.y>]␈↓.
␈↓ ↓H␈↓Case ␈↓↓qat z␈↓:
␈↓ ↓H␈↓ ␈↓↓subst[x,y,z] = qif y=z qthen x qelse z␈↓ ...by definition of ␈↓↓subst␈↓
␈↓ ↓H␈↓ ␈↓↓sublis[z,<y.x>] = {assoc[z,<y.x>]}[λz1: qif qn z1 qthen z qelse qd z1]␈↓ ... by definition of ␈↓↓sublis␈↓
␈↓ ↓H␈↓ ␈↓↓= qif y≠z qthen z qelse qd y.x␈↓ ...by computation since ␈↓↓slist <y.x>␈↓.
␈↓ ↓H␈↓Case ␈↓↓¬qat z␈↓ and ␈↓↓∀x y: [subst[x, y, qa z] = sublis[qa z, <y.x>] ∧ subst[x,y,qd z] = sublis[qd z,<y.x␈↓
␈↓ ↓H␈↓ ␈↓↓subst[x,y,z] = subst[x,y,qa z] . subst[x,y,qd z]␈↓ ...by definition of ␈↓↓subst␈↓
␈↓ ↓H␈↓ ␈↓↓= sublis[qa z, <y.x>] . sublis[qd z,<y.x>]␈↓ ...by induction hypothesis
␈↓ ↓H␈↓ ␈↓↓= sublis[z,<y.x>]␈↓ ...by definition of ␈↓↓sublis.␈↓
␈↓ ↓H␈↓ Before proving (ii) we prove some lemmas. Namely
␈↓ ↓H␈↓2.10 ␈↓↓∀z s1 s2: [qn assoc[z, s1] ⊃ assoc[z, s1@s2] = assoc[z,s2]]␈↓
␈↓ ↓H␈↓2.11 ␈↓↓∀z s1 s2: [¬qn assoc[z,s1] ⊃ ¬qn assoc[z,s1@s2] ∧ qd assoc[z,s1@s2] = sublis[qd assoc[z,s1],␈↓
␈↓ ↓H␈↓These␈αare␈αfairly␈αsimple␈αconsequences␈αof␈αthe␈αfacts␈αmentioned␈αat␈αthe␈αbeginning␈αof␈αthis␈αproblem␈α
and␈↓ ↓H␈↓␈↓ εH␈↓ 94
␈↓ ↓H␈↓the following statement:
␈↓ ↓H␈↓2.12 ␈↓↓∀z s1 s2: [qn assoc[z, s1] ≡ qn assoc[z,subsub[s1,s2]]]␈↓
␈↓ ↓H␈↓ ␈↓↓∧ [¬qn assoc[z,s1] ⊃ qd assoc[z,subsub[s1,s2] = sublis[qd assoc[z,s1],s2]]␈↓
␈↓ ↓H␈↓αProof of 2.12.
␈↓ ↓H␈↓Method: list induction on ␈↓↓s1.␈↓
␈↓ ↓H␈↓Case ␈↓↓qn s1␈↓:
␈↓ ↓H␈↓ Both sides of the equivalence reduce to ␈↓↓qn qNIL␈↓ and the left hand side of ⊃ is F.
␈↓ ↓H␈↓Case ␈↓↓¬qn s1␈↓ and ␈↓↓∀z s2: [qn assoc[z, qd s1] ≡ qn assoc[z,subsub[qd s1,s2]]]␈↓
␈↓ ↓H␈↓ ␈↓↓∀z s2: [¬qn assoc[z,qd s1] ⊃ qd assoc[z,subsub[qd s1,s2] = sublis[qd assoc[z,qd s1], ␈↓
␈↓ ↓H␈↓ ␈↓↓assoc[z,subsub[s1,s2]] = qif z=qaa subsub[s1,s2] qthen qa subsub[s1,s2] qelse assoc[z,subsub[qd ␈↓
␈↓ ↓H␈↓ ...by definition of ␈↓↓assoc␈↓
␈↓ ↓H␈↓ ...here we need ␈↓↓slist subsub[s1,s2]␈↓, ␈↓↓¬qn subsub[s1,s2]␈↓ and ␈↓↓qd subsub[s1,s2] = subsub[qd s1␈↓
␈↓ ↓H␈↓ ␈↓↓= qif z = qaa s1 qthen [qaa s1 . sublis[qda s1,s2]] qelse assoc[z, subsub[qd s1,s2]]␈↓
␈↓ ↓H␈↓ ...here we need in addition, 2.1, the definition of ␈↓↓subsub␈↓ and ␈↓↓issexp sublis[qda s1,s2]␈↓
␈↓ ↓H␈↓Subcase ␈↓↓z = qaa s1 ␈↓: the result follows from the definitions by computation.
␈↓ ↓H␈↓Subcase ␈↓↓z ≠ qaa s1␈↓: the result follows from the induction hypothesis and definition of ␈↓↓assoc.␈↓
␈↓ ↓H␈↓αProof of 2.10
␈↓ ↓H␈↓Assume: ␈↓↓qn assoc[z,s1]␈↓
␈↓ ↓H␈↓ ␈↓↓qn assoc[z, subsub[s1,s2]]␈↓ ... by 2.12
␈↓ ↓H␈↓ ␈↓↓assoc[z,subsub[s1,s2]*s2] = assoc[z,s1@s2] = assoc[z,s2]␈↓ ...by 2.5 and definition of @.
␈↓ ↓H␈↓αProof of 2.11
␈↓ ↓H␈↓Assume: ␈↓↓¬qn assoc[z,s1]␈↓
␈↓ ↓H␈↓ ␈↓↓¬qn assoc[z,subsub[s1,s2]]␈↓ ...by 2.12
␈↓ ↓H␈↓ ␈↓↓assoc[z,s1@s2] = assoc[z,subsub[s1,s2]]␈↓ ...by 2.5 and definition of @
␈↓ ↓H␈↓The result then follows from the second part of 2.12 and ␈↓¬NOTNIL-APPEND. ␈↓
␈↓ ↓H␈↓αProof of 2.ii ␈↓↓∀z s1 s2: sublis[z,s1@s2] = sublis[sublis[z,s1],s2]␈↓α.
␈↓ ↓H␈↓Method: S-expression induction with ␈↓↓qP[z] ≡ ∀s1 s2: sublis[z,s1@s2] = sublis[sublis[z,s1],s2]␈↓.
␈↓ ↓H␈↓Case ␈↓↓qat z␈↓:
␈↓ ↓H␈↓ ␈↓↓sublis[z,s1@s2] = {assoc[z,s1@s2]}[λz1: qif qn z1 qthen z qelse qd z1]␈↓
␈↓ ↓H␈↓ ␈↓↓sublis[z,s1] = {assoc[z,s1]}[λz1: qif qn z1 qthen z qelse qd z1]␈↓
␈↓ ↓H␈↓If ␈↓↓qn assoc[z,s1]␈↓ the result follows from 2.10 and if ␈↓↓¬qn assoc[z,s1]␈↓ the result follows from 2.11.␈↓ ↓H␈↓␈↓ εH␈↓ 95
␈↓ ↓H␈↓Case ␈↓↓¬qat z␈↓ and ␈↓↓∀s2: [sublis[qa z, s1@s2] = sublis[sublis[qa z,s1],s2]␈↓
␈↓ ↓H␈↓ ∧ ␈↓↓∀s2: [sublis[qd z, s1@s2] = sublis[sublis[qd z,s1],s2]␈↓
␈↓ ↓H␈↓ ␈↓↓sublis[z,s1@s2] = sublis[qa z,s1@s2] . sublis[qd z,s1@s2]␈↓ ...by definition
␈↓ ↓H␈↓ ␈↓↓= sublis[sublis[qa z,s1],s2] . sublis[sublis[qd z,s1],s2]␈↓ ...by induction
␈↓ ↓H␈↓ ␈↓↓= sublis[sublis[z,s1],s2]␈↓ ... by definition of ␈↓↓sublis␈↓
␈↓ ↓H␈↓ ...here we need ␈↓↓issexp sublis[qa z,s1]␈↓ and ␈↓↓issexp sublis[qd z,s1]␈↓
␈↓ ↓H␈↓αProof of 2.iii ␈↓↓∀z s1 s2 s3: sublis[z, s1@[s2@s3]] = sublis[z, [s1@s2]@s3]]␈↓α
␈↓ ↓H␈↓ This is a direct consequence of 2.ii and ␈↓↓slist s1@s2␈↓ as follows:
␈↓ ↓H␈↓ ␈↓↓sublis[z, s1@[s2@s3]] = sublis[sublis[z,s1],s2@s3] ␈↓
␈↓ ↓H␈↓ ␈↓↓= sublis[sublis[sublis[z,s1],s2],s3]␈↓
␈↓ ↓H␈↓ ␈↓↓= sublis[sublis[z,s1@s2],s3]␈↓
␈↓ ↓H␈↓ ␈↓↓= sublis[z, [s1@s2]@s3]␈↓
␈↓ ↓H␈↓αProof of 2.iv ␈↓↓∀x y z: [¬occur[y,z] ⊃ subst[x,y,z] = z]␈↓α
␈↓ ↓H␈↓Method: S-expression induction with ␈↓↓qP[z] ≡ ∀x y: [¬occur[y,z] ⊃ subst[x,y,z] = z]␈↓.
␈↓ ↓H␈↓Case ␈↓↓qat z␈↓:
␈↓ ↓H␈↓ ␈↓↓¬occur[y,z] ≡ y≠z␈↓ and ␈↓↓subst[x,y,z] = qif y = z qthen x qelse z␈↓ so qP holds.
␈↓ ↓H␈↓Case ␈↓↓¬qat z␈↓ and ␈↓↓∀x y: [¬occur[y, qa z] ⊃ subst[x,y,qa z] = qa z ∧ [¬occur[y, qd z] ⊃ subst [x,y,qd␈↓
␈↓ ↓H␈↓ ␈↓↓¬occur[y,z] ≡ y≠z ∧ ¬occur[y,qa z] ∧ ¬occur[y,qd z]␈↓
␈↓ ↓H␈↓ ␈↓↓subst[x,y,z] = subst[x,y,qa z] . subst[x,y,qd z]␈↓ ...by definition
␈↓ ↓H␈↓ ␈↓↓= qa z . qd z␈↓ ...by induction hypothesis
␈↓ ↓H␈↓ ␈↓↓= z␈↓
␈↓ ↓H␈↓␈↓αProof of 2.v␈↓ ␈↓↓∀x x1 y y1 z: [y ≠ y1 ∧ ¬occur[y, x1]] ⊃ ␈↓
␈↓ ↓H␈↓ ␈↓↓subst[x1,y1,subst[x,y,z]] = subst[subst[x1,y1,x],y,subst[x1,y1,z]]␈↓
␈↓ ↓H␈↓Method: S-expression induction on ␈↓↓z.␈↓
␈↓ ↓H␈↓Case ␈↓↓qat z␈↓:
␈↓ ↓H␈↓ ␈↓↓subst[x1,y1,subst[x,y,z]] = qif y=z qthen subst[x1,y1,x] qelse qif y1=z qthen x1 qelse z␈↓
␈↓ ↓H␈↓ ␈↓↓subst[subst[x1,y1,x],y,subst[x1,y1,z]] ␈↓
␈↓ ↓H␈↓ ␈↓↓= qif y1=z qthen qif y=x1 qthen subst[x1,y1,x] qelse x1␈↓
␈↓ ↓H␈↓ ␈↓↓qelse qif y=z qthen subst[x1,y1,x] qelse z␈↓
␈↓ ↓H␈↓ ␈↓↓=qif y1=z qthen x1 qelse qif y=z qthen subst[x1,y1,x] qelse z␈↓ ...since ␈↓↓¬occur[y,x1]␈↓
␈↓ ↓H␈↓The result now follows by a simple case analysis since ␈↓↓y=z␈↓ and ␈↓↓y1=z␈↓ can not both be true.
␈↓ ↓H␈↓Case ␈↓↓¬qat z␈↓ and ␈↓↓∀x x1 y y1: [y ≠ y1 ∧ ¬occur[y, x1]] ⊃␈↓
␈↓ ↓H␈↓ ␈↓↓subst[x1,y1,subst[x,y,qa z] = subst[subst[x1,y1,x],y,subst[x1,y1,qa z]]␈↓
␈↓ ↓H␈↓ ␈↓↓∧ subst[x1,y1,subst[x,y,qd z] = subst[subst[x1,y1,x],y,subst[x1,y1,qd z]]]␈↓
␈↓ ↓H␈↓ ␈↓↓subst[x1,y1,subst[x,y,z]] = subst[x1,y1,subst[x,y,qa z] . subst[x,y,qd z]]␈↓␈↓ ↓H␈↓␈↓ εH␈↓ 96
␈↓ ↓H␈↓ ␈↓↓= subst[x1,y1,subst[x,y,qa z]] . subst[x1,y1,[subst[x,y,qd z]]␈↓
␈↓ ↓H␈↓ ...here we need ␈↓↓issexp subst[x,y,qa z]␈↓ and ␈↓↓issexp subst[x,y,qd z]␈↓
␈↓ ↓H␈↓ ␈↓↓= subst[subst[x1,y1,x],y,subst[x1,y1,qa z]] . subst[subst[x1,y1,x],y,subst[x1,y1,qd ␈↓
␈↓ ↓H␈↓ ␈↓↓= subst[subst[x1,y1,x],y,subst[x1,y1,z]]␈↓
␈↓ ↓H␈↓This completes problem 2.
␈↓ ↓H␈↓αProblem 3.
␈↓ ↓H␈↓ We wish to prove the following two statements:
␈↓ ↓H␈↓(i) ␈↓↓∀u v: andlis[u*v,phi] ≡ andlis[u,phi] ∧ andlis[v,phi]␈↓
␈↓ ↓H␈↓(ii) ␈↓↓∀u: andlis[u,phi] ≡ andlis[reverse u,phi]␈↓
␈↓ ↓H␈↓where␈α∂␈↓↓phi␈↓␈α∂is␈α∂a␈α∂unary␈α∂predicate.␈α∂ (The␈α∂use␈α∂of␈α∂␈↓↓p␈↓␈α∂in␈α∂the␈α∂original␈α∂porblem␈α∂statement␈α∂was␈α⊂a␈α∂poor
␈↓ ↓H␈↓choice␈α
as␈α
␈↓↓p␈↓␈α
is␈α∞designated␈α
in␈α
Chapter␈α
3␈α
as␈α∞a␈α
variable␈α
of␈α
type␈α
␈↓↓istv.)␈↓␈α∞ Note␈α
that␈α
even␈α
to␈α∞state␈α
this
␈↓ ↓H␈↓problem␈α
requires␈αan␈α
extension␈αto␈α
the␈αsyntax␈α
of␈α
our␈αlanguage␈α
in␈αorder␈α
to␈αallow␈α
functions␈αthat␈α
have
␈↓ ↓H␈↓functions␈α
as␈α
arguments.␈α
In␈α∞the␈α
problem␈α
␈↓↓phi␈↓␈α
is␈α∞considered␈α
as␈α
a␈α
parameter.␈α∞ (Quantification␈α
over
␈↓ ↓H␈↓predicates is not allowed.)
␈↓ ↓H␈↓ The␈α
strategy␈α
for␈α
doing␈αthe␈α
proof␈α
is␈α
as␈α
follows.␈α We␈α
define␈α
a␈α
representing␈α
function␈α␈↓↓aandlis␈↓
␈↓ ↓H␈↓for␈α∩␈↓↓andlis.␈↓␈α⊃ To␈α∩do␈α⊃this␈α∩we␈α⊃need␈α∩to␈α∩know␈α⊃that␈α∩␈↓↓phi␈↓␈α⊃has␈α∩a␈α⊃representing␈α∩function␈α∩␈↓↓pphi.␈↓␈α⊃ The
␈↓ ↓H␈↓statement␈α∩that␈α∩␈↓↓phi␈↓␈α∩is␈α∪suitable␈α∩well␈α∩behaved␈α∩becomes␈α∩then␈α∪the␈α∩statement␈α∩that␈α∩␈↓↓pphi␈↓␈α∪maps␈α∩S-
␈↓ ↓H␈↓expressions into the domain ␈↓¬TV ␈↓and maps general objects into the domain ␈↓¬ETV. ␈↓ Thus
␈↓ ↓H␈↓3.1 ␈↓↓∀u: [aandlis[u,pphi] = nnull u oor [pphi qa u aand aandlis[qd u,pphi]]␈↓
␈↓ ↓H␈↓3.2 ␈↓↓∀u: isetv aandlis qd u␈↓
␈↓ ↓H␈↓3.3 ␈↓↓∀u: isetv pphi qa u␈↓
␈↓ ↓H␈↓3.4 ␈↓↓∀x: istv pphi x␈↓
␈↓ ↓H␈↓3.5 ␈↓↓∀x: [phi x ≡ pphi x=␈↓¬TT␈↓↓]␈↓
␈↓ ↓H␈↓3.6 ␈↓↓∀u: [andlis[u,phi] ≡ aandlis[u,pphi] = ␈↓¬TT␈↓↓]␈↓
␈↓ ↓H␈↓Here␈α∞␈↓↓nnull␈↓␈α
is␈α∞defined␈α∞similarly␈α
to␈α∞␈↓↓aatom␈↓␈α
and␈α∞we␈α∞assume␈α
the␈α∞analagous␈α
results␈α∞such␈α∞as␈α
␈↓¬TVNNUL,
␈↓ ↓H␈↓¬␈↓and␈α␈↓¬EQNNUL.␈α␈↓␈α3.2␈αand␈α3.3␈αare␈αneeded␈αinorder␈αto␈αbe␈αable␈αto␈αuse␈αthe␈αdefinitions␈αof␈α␈↓↓aand␈↓␈αand␈α␈↓↓oor␈↓␈αin
␈↓ ↓H␈↓the case ␈↓↓qn u␈↓. Using these axioms we prove
␈↓ ↓H␈↓3.7 ␈↓↓∀u: istv aandlis[u,pphi]␈↓
␈↓ ↓H␈↓from which we get (using ␈↓¬EQAAND ␈↓␈↓¬EQOOR ␈↓etc., and the above axioms) that
␈↓ ↓H␈↓3.8 ␈↓↓∀u: [andlis[u,phi] ≡ qn u ∨ [phi qa u ∧ andlis[qd u,phi]]␈↓.
␈↓ ↓H␈↓This last statement is used together with list induction to prove the desired results.
␈↓ ↓H␈↓αProof of 3.7
␈↓ ↓H␈↓Method: list induction with ␈↓↓qP[u] ≡ istv aandlis[u,pphi]␈↓.
␈↓ ↓H␈↓Case ␈↓↓qn u␈↓:
␈↓ ↓H␈↓ ␈↓↓istv aandlis[u,pphi] ≡ istv ␈↓¬TT␈↓↓␈↓ ...by definitions of ␈↓↓nnull,␈↓ ␈↓↓aand,␈↓ ␈↓↓oor,␈↓ 3.1, 3.2 and 3.3 .
␈↓ ↓H␈↓Case ␈↓↓¬qn u␈↓ and ␈↓↓istv aandlis[qd u,pphi]␈↓:
␈↓ ↓H␈↓ ␈↓↓istv aandlis[u,pphi]␈↓ follows by definition and ␈↓¬TVOOR ␈↓from␈↓ ↓H␈↓␈↓ εH␈↓ 97
␈↓ ↓H␈↓ ␈↓↓[istv nnull u]∧[istv [pphi qa u aand aandlis[qd u,pphi]]␈↓
␈↓ ↓H␈↓but we have
␈↓ ↓H␈↓ ␈↓↓istv [pphi qa u aand aandlis[qd u,pphi]␈↓ ...by induction, ␈↓¬TVAND ␈↓and 3.4
␈↓ ↓H␈↓ ␈↓↓istv [nnull u]␈↓ ..by remarks above
␈↓ ↓H␈↓αProof of 3.i.
␈↓ ↓H␈↓Method: list induction with ␈↓↓qP[u] ≡ ∀v: [andlis[u*v,phi] ≡ andlis[u,phi] ∧ andlis[v,phi]]␈↓
␈↓ ↓H␈↓Case ␈↓↓qn u␈↓:
␈↓ ↓H␈↓ ␈↓↓andlis[u*qNIL,phi] ≡ andlis[u,phi]␈↓ ...by ␈↓¬NIL-APPEND ␈↓
␈↓ ↓H␈↓ ␈↓↓≡ andlis[u,phi] ∧ andlis[qNIL,phi]␈↓ ...by 3.8
␈↓ ↓H␈↓Case ␈↓↓¬qn u␈↓ and ␈↓↓∀v: andlis[qd u*v,phi] ≡ andlis[qd u,phi] ∧ andlis[v,phi]␈↓
␈↓ ↓H␈↓ ␈↓↓andlis[u*v,phi] ≡ phi qa u ∧ andlis[qd u*v,phi]␈↓ ...by ␈↓¬CAR/CDR-APPEND, ␈↓␈↓¬ISTOT-APPEND, ␈↓a
␈↓ ↓H␈↓ ␈↓↓≡ phi qa u ∧ andlis[qd u,phi] ∧ andlis[v,phi]␈↓ ...by the induction hypothesis
␈↓ ↓H␈↓ ␈↓↓≡ andlis[u,phi] ∧ andlis[v,phi]␈↓ ...by 3.8.
␈↓ ↓H␈↓αProof of 3.ii .
␈↓ ↓H␈↓Method: list induction with ␈↓↓qP[u] ≡ [andlis[u,phi] ≡ andlis[reverse u,phi]]␈↓.
␈↓ ↓H␈↓Case ␈↓↓qn u␈↓:
␈↓ ↓H␈↓ ␈↓↓andlis[reverse qNIL,phi] ≡ andlis[qNIL,phi]␈↓ ...by definition of ␈↓↓reverse␈↓
␈↓ ↓H␈↓Case ␈↓↓¬qn u␈↓ and ␈↓↓andlis[reverse qd u,phi] ≡ andlis[qd u,phi]␈↓:
␈↓ ↓H␈↓ ␈↓↓andlis[reverse u,phi] ≡ andlis[reverse qd u * <qa u>,phi]␈↓ ...by definition of ␈↓↓reverse␈↓
␈↓ ↓H␈↓ ␈↓↓≡ andlis[reverse qd u,phi] ∧ andlis[<qa u>,phi]␈↓ ...by (i)
␈↓ ↓H␈↓ ...here we need ␈↓↓islist reverse qd u␈↓ and ␈↓↓islist <qa u>␈↓
␈↓ ↓H␈↓ ␈↓↓≡ andlis[<qa u>,phi] ∧ andlis[qd u,phi]␈↓ ...by induction hypothesis
␈↓ ↓H␈↓ ␈↓↓≡ andlis[u,phi]␈↓ ...by 3.8 and properties of <>.
␈↓ ↓H␈↓This completes Problem 3.